fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
FAC(s(x)) → *1(s(x), fac(x))
FAC(s(x)) → FAC(x)
+1(x, s(y)) → +1(x, y)
FLOOP(s(x), y) → FLOOP(x, *(s(x), y))
FLOOP(s(x), y) → *1(s(x), y)
*1(x, s(y)) → *1(x, y)
FAC(0) → 11
*1(x, s(y)) → +1(*(x, y), x)
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
FAC(s(x)) → *1(s(x), fac(x))
FAC(s(x)) → FAC(x)
+1(x, s(y)) → +1(x, y)
FLOOP(s(x), y) → FLOOP(x, *(s(x), y))
FLOOP(s(x), y) → *1(s(x), y)
*1(x, s(y)) → *1(x, y)
FAC(0) → 11
*1(x, s(y)) → +1(*(x, y), x)
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
+1(x, s(y)) → +1(x, y)
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(x, s(y)) → +1(x, y)
The value of delta used in the strict ordering is 1/16.
POL(s(x1)) = 1/4 + (2)x_1
POL(+1(x1, x2)) = (1/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
*1(x, s(y)) → *1(x, y)
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(x, s(y)) → *1(x, y)
The value of delta used in the strict ordering is 8.
POL(*1(x1, x2)) = (2)x_2
POL(s(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
FLOOP(s(x), y) → FLOOP(x, *(s(x), y))
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FLOOP(s(x), y) → FLOOP(x, *(s(x), y))
The value of delta used in the strict ordering is 2.
POL(FLOOP(x1, x2)) = (4)x_1
POL(*(x1, x2)) = 0
POL(s(x1)) = 1/2 + x_1
POL(0) = 0
POL(+(x1, x2)) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
FAC(s(x)) → FAC(x)
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FAC(s(x)) → FAC(x)
The value of delta used in the strict ordering is 1/16.
POL(FAC(x1)) = (1/4)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
fac(0) → 1
fac(s(x)) → *(s(x), fac(x))
floop(0, y) → y
floop(s(x), y) → floop(x, *(s(x), y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
1 → s(0)
fac(0) → s(0)